/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.transform;

import java.util.HashMap;
import java.util.Iterator;
import java.util.Map;

import alloy.ast.ASTDepthFirstVisitor;
import alloy.ast.CheckCommand;
import alloy.ast.Decls;
import alloy.ast.FindCommand;
import alloy.ast.Formula;
import alloy.ast.FormulaPara;
import alloy.ast.FormulaSeq;
import alloy.ast.Formulas;
import alloy.ast.Function;
import alloy.ast.InvocablePara;
import alloy.ast.Module;
import alloy.ast.Node;
import alloy.ast.QuantifiedFormula;
import alloy.ast.Quantifier;
import alloy.ast.RunCommand;
import alloy.ast.Signature;
import alloy.ast.Specification;
import alloy.semantic.CheckHigherOrderQuantifiersVisitor;
import alloy.util.Dbg;
import alloy.util.Params;

/**
 * A visitor which generates full formulas for each command in a Specification's focus module.
 * The formula for each command includes: the body of function / predicate / assertion referred to
 * in the command, all global facts, and all formulas implicit in Signature declarations.
 */
public class GenCommandFormulasVisitor extends ASTDepthFirstVisitor {

    /** keep pointer to spec for generating mega-fact */
    Specification _spec;

    /**[QualifiedName->Signature] maps signature names to corresponding
     * Signatures for all Signatures in _spec **/
    Map _sigNameToSig;

    /** ImplicitConstraintGenerator used to generate implicit constraints for _spec **/
    ImplicitConstraintGenerator _icg = new ImplicitConstraintGenerator();

    public void visit(Specification spec_) {
       _spec = spec_;

       // generate sig name to sig mapping
       _sigNameToSig = _getNameToSigMap(_spec);

       // generate the implicit constraints for all signatures in _spec
       _icg.createSigConstraints(_sigNameToSig.values());

       // visit _spec's focus module:  we intentionally left out other modules
       // because their commands do not need to be processed
       visit((Node)spec_.getFocus());
    }


    private static Map _getNameToSigMap(Specification spec_) {
        Map map = new HashMap();
        Iterator moduleIter = spec_.getModules().getModuleIter();

        while (moduleIter.hasNext()) {
            Iterator sigIter = ((Module) moduleIter.next()).getSignatures().getSignatureIter();
            while (sigIter.hasNext()) {
            Signature sig = (Signature) sigIter.next();
            Dbg.check(!map.containsKey(sig.getName()));
            map.put(sig.getName(), sig);
            }
        }

        return map;
    }

    public void visit(FindCommand findCommand_) {

        findCommand_.leafIdToMult = _icg.leafIdToMult;

        // construct the megafact:  a formula which includes all global facts
        // and all constraints implied by Signature declarations
        MegaFactVisitor mfv = new MegaFactVisitor(_icg.sigToConstraints);
        _spec.applyVisitor(mfv);
        FormulaSeq megaFact = mfv.getMegaFact();

        // add the megafact to findCommand_'s basic formula
        if (!megaFact.getFormulas().isLeaf()) {
            megaFact.annotate("all global constraints");
            Formulas formulas = new Formulas();

            formulas.addFormula(findCommand_.formula);
            formulas.addFormula(megaFact);

            findCommand_.formula = new FormulaSeq(formulas);
        }
      
        
        // optimize and desugare the final formula
        findCommand_.formula = _applyOptimizationsAndDesugar(findCommand_);
        
    }

    public void visit(RunCommand runCommand_) {

    // generate the formula for the body of the function / predicate referenced in runCommand_
    FormulaPara para = runCommand_.getFormulaPara(_spec.getFocus().getModuleInfo());

    // if the function/predicate doesn't exist, nothing do to
        if (para != null) {

        // need to existentially quantify over arguments, if any
        InvocablePara invocable = (InvocablePara) para;
        Decls argDecls = (Decls) invocable.getArgList().getArgDecls().copy();

        // if function, also existentially quantify over return value
        if (invocable instanceof Function) {
        argDecls.addDecl(((Function)invocable).getReturnDecl());
        }

        if (!argDecls.isLeaf()) {
        runCommand_.formula = new QuantifiedFormula(Quantifier.SOME,
                                argDecls,
                                (Formula) para.getFormula().copy(), true);
        } else {
        runCommand_.formula = (Formula) para.getFormula().copy();
        }

        runCommand_.formula.annotate("formula for function " +
                     runCommand_.invocablePara.getName().nodeString());

        visit((FindCommand) runCommand_);
    }
    }

    public void visit(CheckCommand checkCommand_) {

    // generate the formula for the body of the assertion referenced in checkCommand_
    FormulaPara para = checkCommand_.getFormulaPara(_spec.getFocus().getModuleInfo());

    // if the assertion doesn't exist, nothing to do
        if (para != null) {

        // negate the assertion's its formula
        checkCommand_.formula = ((Formula) para.getFormula().copy()).not();

        checkCommand_.formula.annotate("negated formula for assertion " +
                       checkCommand_.assertionPara.getName().nodeString());

        visit((FindCommand) checkCommand_);

    }
    }


    private Formula _applyOptimizationsAndDesugar(FindCommand command) {
        Formula formulaSeq = command.formula;

      
        
        // THIS IS BROKEN:  DO NOT UNCOMMENT
//        if (Params.glob.getBoolParam("DEVEL", "quantremover")) {
//        formulaSeq = (Formula) QuantifierRemover.removeQuantifiers(formulaSeq, command);
//        }
        
              formulaSeq.applyReturnVisitor(new DesugarOverrideVisitor());
       
        
        // desugar multiplicity formulas
        formulaSeq.applyReturnVisitor(new DesugarMultFormulasVisitor());

        // desugar quantifiers
        formulaSeq.applyReturnVisitor(new DesugarQuantifiersVisitor());

        // desugar declarations
        formulaSeq.applyVisitor(new DesugarDeclsVisitor());

        // desugar quantifiers generated in declaration constraints
        formulaSeq.applyReturnVisitor(new DesugarQuantifiersVisitor());

        //System.out.println("FORMULA AFTER DESUGARINGS OF QUANTIFIERS & DECLS");
        //System.out.println(formulaSeq.nodeString());

        // don't continue if Int was found
        if (alloy.util.Dbg.userError) return null;

        // set leaf ids
        command.sliv = new SetLeafIdsVisitor(command.leafIdToMult, _sigNameToSig);
        formulaSeq.applyVisitor(command.sliv);

      
        if (Params.glob.getBoolParam("MAIN", "skolemize")) {
            // skolemize
            formulaSeq = SkolemizationVisitor.skolemize(formulaSeq, command.leafIdToMult);
	    command.sliv.setSkolemLeafIdMap(SkolemizationVisitor.skolemLeafIdMap.copy());
	    //System.out.println("new cmd: " + command);
	    //System.out.println("new sliv: " + command.sliv);
	    command.skolemIds = SkolemizationVisitor.skolemLeafIds;
	    command.skolemTypes = SkolemizationVisitor.skolemTypes;
	    command.skolemMap = SkolemizationVisitor.skolemLeafIdMap.copy();
        }

        formulaSeq.applyVisitor(new SimplifyVisitor());

        // set leaf ids again to handle skolem functions
        formulaSeq.applyVisitor(command.sliv);

        // no higher-order quantifiers
        if (!Params.glob.getBoolParam("MAIN", "allowhigherorder")) {
            formulaSeq.applyVisitor(new CheckHigherOrderQuantifiersVisitor());
        }

        return (formulaSeq instanceof FormulaSeq ? formulaSeq :
            new FormulaSeq(new Formulas(formulaSeq)));
    }
}







